Nuprl Lemma : es-interface-image-trivial
11,40
postcript
pdf
es
:ES,
A
:Type,
Ia
:AbsInterface(
A
).
e
.
e
'
Ia
=
Ia
latex
Definitions
t
T
,
Top
,
x
:
A
.
B
(
x
)
Lemmas
es-is-interface-image
origin
es:ES, A:Type, Ia:AbsInterface(A). 
e.e'Ia = Ia es:ES, A:Type, Ia:AbsInterface(A). e.e'Ia = Ia 
Tx:A. B(x)